n, m:. firstn(n;upto(m)) ~ if n z m then upto(n) else upto(m) fi  

latex

Definitions	x:A. B(x), if b then t else f fi , t  T, P  Q, tt, P  Q, , P & Q, P  Q, ff, T, True, {i..j}, i  j < k, Top, S  T, A  B, A, False, , , Unit,
Lemmas	le int wf, bool wf, iff transitivity, assert wf, le wf, eqtt to assert, assert of le int, lt int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int, nat wf, upto decomp, firstn append, upto wf, top wf, int seg wf, map wf, length upto, firstn all